\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$, $B$:Type, ${\it Ias}$:(AbsInterface($A$) List), ${\it Ibs}$:(AbsInterface($B$) List),\+
\\[0ex]$f$:(E(p{-}first(${\it Ias}$))$\rightarrow$$B$).
\-\\[0ex]($\forall$${\it Ia}_{1}$,${\it Ia}_{2}$$\in$${\it Ias}$.  $\forall$$e$, ${\it e'}$:E. ($\uparrow$($e$ $\in_{b}$ ${\it Ia}_{1}$)) $\Rightarrow$ ($\uparrow$(${\it e'}$ $\in_{b}$ ${\it Ia}_{2}$)) $\Rightarrow$ ($\neg$(loc($e$) = loc(${\it e'}$) $\in$ Id)))
\\[0ex]$\Rightarrow$ ($\forall$${\it Ib}_{1}$,${\it Ib}_{2}$$\in$${\it Ibs}$.  ${\it Ib}_{1}$ $\cap$ ${\it Ib}_{2}$ = 0)
\\[0ex]$\Rightarrow$ ($\parallel$${\it Ias}$$\parallel$ = $\parallel$${\it Ibs}$$\parallel$ $\in$ $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ ($\forall$$i$:\{0..$\parallel$${\it Ias}$$\parallel^{-}$\}. glued(${\it es}$; $B$; $f$; ${\it Ias}$[$i$]; ${\it Ibs}$[$i$]))
\\[0ex]$\Rightarrow$ glued(${\it es}$; $B$; $f$; p{-}first(${\it Ias}$); p{-}first(${\it Ibs}$))
\end{tabbing}